ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A), es:ES, e:E.
es-decl(es;ds;da)  (in-interface(es;X;e))  (interface-val(es;X;e)  (A + Top)) 

latex

Definitions

Type, ES, E, es-decl(es;ds;da), Interface(ds;da;A), interface-val(es;X;e), s = t, x.A(x), a:A fp B(a), EqDecider(T), locknd-deq(), x,y. t(x;y), {x:A| B(x)} , b, hasloc(k;i), S  T, LocKnd, x. t(x), P  Q, f(x), <a, b>, loc(e), kind(e), x:A  B(x), Knd, Id, left + right, Top, let i,k:LocKnd = ik in P(i;k), (state when e), state@i, x:A. B(x), x:AB(x), val(e), t  T, f(a), valtype(e), in-interface(es;X;e), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , t.1, x  dom(f), SQType(T), s ~ t, {T}, P & Q, A c B, x:A.B(x), Void, kindtype(i;k)

Lemmas

es-valtype-kindtype, LocKnd wf, fpf-dom wf, es-hasloc, es-val wf, es-state-when wf, top wf, fpf-ap wf, hasloc wf, assert wf, locknd-spread wf2, locknd-deq wf, fpf-trivial-subtype-top, es-kind wf, es-loc wf, Knd wf, Id wf